Nuprl Lemma : rel-immediate_functionality_wrt_breqv
11,40
postcript
pdf
T
:Type,
R
,
Q
:(
T
T
). (
R
<
>{
T
}
Q
)
(
R
! <
>{
T
}
Q
!)
latex
Definitions
E
<
>{
T
}
E'
Lemmas
rel-immediate
functionality
wrt
iff
origin
T:Type, R, Q:(T
T
). (R <
>{T} Q) 
(R! <>{T} Q!) T:Type, R, Q:(TT). (R <>{T} Q) (R! <>{T} Q!) >{T} E'